package com.googlecode.kipler.satisfiability.interpolation.rule;

import java.util.LinkedHashSet;
import java.util.Set;

import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.Formula;

public abstract class InterpolantRule {

	private Set<Formula> condition = new LinkedHashSet<Formula>();

	private Set<ConceptAssertion> previousInterpolants = new LinkedHashSet<ConceptAssertion>();

	private WorldConstraintSystem wcs;

	public abstract ConceptAssertion apply();

	public InterpolantRule() {
		super();
	}

	public WorldConstraintSystem getWcs() {
		return wcs;
	}

	public void setWcs(WorldConstraintSystem wcs) {
		this.wcs = wcs;
	}

	public Set<Formula> getCondition() {
		return condition;
	}

	public void setCondition(Set<Formula> condition) {
		this.condition = condition;
	}
	
	public void addCondition(Formula condition) {
		this.condition.add(condition);
	}

	public Set<ConceptAssertion> getPreviousInterpolants() {
		return previousInterpolants;
	}

	public void addPreviousInterpolant(ConceptAssertion previousInterpolant) {
		previousInterpolants.add(previousInterpolant);
	}

}